forall a: forall b:
L:a,b^ = L:b,a